M1, M2:MsgA. M1  M1  M2 

latex

Definitions	x:A. B(x), M1  M2, M1  M2, State(ds), Valtype(da;k), Prop, 1of(t), 2of(t), A & B, P & Q, mk-ma, t  T, x. t(x), MsgA, x(s), P  Q
Lemmas	fpf-sub-join-left, Id wf, id-deq wf, Knd wf, Kind-deq wf, fpf-cap wf, fpf-join wf, subtype-fpf2, subtype-fpf-cap-void, ma-state wf, locl wf, top wf, subtype rel function, subtype rel dep function, subtype rel self, subtype-fpf-cap-top, pi1 wf, pi2 wf, product-deq wf, IdLnk wf, rcv wf, idlnk-deq wf, subtype rel list, subtype rel product, msga wf